Nuprl Lemma : neg_assert_of_eq_atom
9,38
postcript
pdf
x
,
y
:Atom. (
(
x
=a
y
))
x
y
Atom
latex
ProofTree
Definitions
a
b
T
,
,
t
T
,
P
Q
,
P
Q
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
nequal
wf
,
eq
atom
wf
,
assert
wf
,
not
wf
origin
x,y:Atom. (
(
x =a y)) 
x 
y 
Atom
x,y:Atom. ((x =a y)) x y Atom
b T 
T Q Q
Q Qx:A. B(x)